\begin{tabbing}
d{-}world\=\{i:l\}\+
\\[0ex]($D$; $v$; ${\it sched}$; ${\it dec}$; ${\it discrete}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$<\lambda$$i$,$x$. d{-}m($D$; $i$).ds($x$)\+
\\[0ex], $\lambda$$i$,$a$. d{-}m($D$; $i$).da(locl($a$))
\\[0ex], $\lambda$$l$,${\it tg}$. d{-}m($D$; source($l$)).dout($l$,${\it tg}$)
\\[0ex], $\lambda$$i$,$t$. if ($t$ =$_{0}$ 0)
\\[0ex]then $\lambda$$x$.d{-}m($D$; $i$).init($x$)?$v$($i$,$x$)
\\[0ex]else (CV(d{-}comp($D$; $v$; ${\it sched}$; ${\it dec}$; ${\it discrete}$))(($t$ {-} 1),$i$)).1
\\[0ex]fi 
\\[0ex], $\lambda$$i$,$t$. ((CV(d{-}comp($D$; $v$; ${\it sched}$; ${\it dec}$; ${\it discrete}$))($t$,$i$)).2).1
\\[0ex], $\lambda$$i$,$t$. (CV(d{-}comp($D$; $v$; ${\it sched}$; ${\it dec}$; ${\it discrete}$))($t$,$i$)).2.2
\\[0ex], $\lambda$$i$.d{-}machine($i$;d{-}m($D$; $i$);${\it dec}$($i$))
\\[0ex], ${\it discrete}$
\\[0ex], $\cdot>$
\-
\end{tabbing}